#include "randombinding.h"

#include "../arc.h"
#include "../expression.h"
#include "../expressions/expressioncommon.h"
#include "../place.h"
#include "../transition.h"
#include "../types/multiset.h"
#include "../types/timedmultiset.h"
#include "../utils/typefactory.h"
#include "binding.h"
#include "bindingalgorithmhelper.h"

using namespace wfnet;

class ConstraintHolder
{
public:
    ConstraintHolder(const VariableName& var = QString()) : m_var(var),
        m_isTimed(false),
        m_simpleConstraints(),
        m_complexConstraints()
    {}
    ~ConstraintHolder() {}

public:
    VariableName m_var;
    bool m_isTimed;
    QSet<const Arc* > m_simpleConstraints;
    QSet<const Arc* > m_complexConstraints;
};

RandomBinding::RandomBinding() : IBindingAlgorithm()
{

}

RandomBinding::~RandomBinding()
{

}

bool RandomBinding::bind(Binding& binding,
    const core::BasicTime& globalClock,
    core::BasicTime& proposedGlobalClock,
    const QSet<const Arc* >& inputArcs,
    const Transition* transition) const
{
    Q_ASSERT(transition != 0);

    bool ret = true;

    QHash<VariableName, ConstraintHolder> constraintMapping;

    // make constraints
    foreach (const Arc* arc, inputArcs)
    {
        Expression* expr = dynamic_cast<Expression* >(
            arc->getExpression());
        const QSet<VariableName> names =
            expr->getUserVariables().keys().toSet();

        foreach (const VariableName& var, names)
        {
            if (constraintMapping.contains(var))
            {
                ConstraintHolder& holder = constraintMapping[var];

                if ((expr->getExpressionType() & SIMPLE_VAR_ONLY) ==
                    SIMPLE_VAR_ONLY)
                {
                    holder.m_simpleConstraints << arc;
                }
                else
                {
                    holder.m_complexConstraints << arc;
                }

                holder.m_isTimed = holder.m_isTimed ||
                    arc->getPlace()->getColorSet()->isTimed();
            }
            else
            {
                ConstraintHolder holder(var);

                if ((expr->getExpressionType() & SIMPLE_VAR_ONLY) ==
                    SIMPLE_VAR_ONLY)
                {
                    holder.m_simpleConstraints << arc;
                }
                else
                {
                    holder.m_complexConstraints << arc;
                }

                holder.m_isTimed = holder.m_isTimed ||
                    arc->getPlace()->getColorSet()->isTimed();

                constraintMapping[var] = holder;
            }
        }
    }

    proposedGlobalClock = 0;
    core::BasicTime _proposedGlobalClock;

    foreach (const ConstraintHolder& holder, constraintMapping)
    {
        const QList<const Arc* > arcs = holder.m_simpleConstraints.toList();

        if (holder.m_simpleConstraints.size() == 1 &&
            holder.m_complexConstraints.size() == 0)
        {
            const Arc* arc = arcs[0];

            BasicTime _globalClock = globalClock;
            _globalClock.add(transition->getDelay().getTime());

            ret = BAH->bindFreeVariable(holder.m_var, arc,
                binding, globalClock, _proposedGlobalClock);

            if (!ret)
            {
                break;
            }

            if (_proposedGlobalClock > proposedGlobalClock)
            {
                proposedGlobalClock = _proposedGlobalClock;
            }
        }
        else
        {
            if (!holder.m_isTimed)
            {
                Multiset intersectedMt;

                BAH->getInstersection(arcs, intersectedMt);

                if (intersectedMt.size() > 0)
                {
                    const int bigtetSize = 32;
                    const int bitarraySize = (intersectedMt.size() /
                        bigtetSize) + 1;

                    int* bitarray = new int[bitarraySize]();

                    bool bindable = false;

                    for (uint i = 0; i < intersectedMt.size() &&
                        !bindable; ++i)
                    {
                        int index = BAH->randomMultisetValue(
                            intersectedMt.size()) + 1;

                        while (BAH->checkBitInBitArray(bitarray, index))
                        {
                            index = BAH->randomMultisetValue(
                                intersectedMt.size());
                        }

                        ColorSet value = intersectedMt.at(index - 1);
                        binding.addBoundVariable(holder.m_var,
                            *value.getType());

                        bool binded = true;

                        foreach (const Arc* arc, holder.m_complexConstraints)
                        {
                            Expression* expr = dynamic_cast<Expression* >(
                                arc->getExpression());
                            expr->setBinding(binding);

                            IMultiset* imt = arc->eval();

                            const Multiset* emt = 0;

                            bool isEvaluatedMsSmaller = false;

                            if (imt->isTimed())
                            {
                                Q_ASSERT(false); // timed/untimed mismatch
                            }
                            else
                            {
                                emt = dynamic_cast<const Multiset* >(imt);

                                const Multiset* pmt =
                                    dynamic_cast<const Multiset* >(
                                        arc->getPlace()->getTokens());

                                Q_ASSERT(pmt != 0 && emt != 0);

                                isEvaluatedMsSmaller = *emt <= *pmt;

                                delete emt;
                            }

                            if (isEvaluatedMsSmaller)
                            {
                                binded = binded && true;
                            }
                            else
                            {
                                BAH->setBitInBitArray(bitarray, index);
                                binded = false;

                                binding.removeBoundVariable(holder.m_var);
                                break;
                            }
                        }

                        if (binded)
                        {
                            if (transition->getGuard() != 0)
                            {
                                Expression* expr = dynamic_cast<Expression* >(
                                    transition->getGuard());
                                expr->setBinding(binding);

                                bindable = transition->check();
                            }
                            else
                            {
                                bindable = true;
                            }
                        }
                    }

                    delete[] bitarray;

                    if (!bindable)
                    {
                        ret = false;
                        break;
                    }
                }
                else
                {
                    ret = false;
                    break;
                }
            }
            else
            {
                const BasicTime transitionDelay = transition->getDelay();

                TimedMultiset intersectedMt;

                BAH->getInstersection(arcs, intersectedMt);

                if (intersectedMt.size() > 0)
                {
                    const int bigtetSize = 32;
                    const int bitarraySize = (intersectedMt.size() /
                        bigtetSize) + 1;

                    int* bitarray = new int[bitarraySize]();

                    bool bindable = false;

                    const QList<QPair<ColorSet, BasicTime> > randomCandidates
                    = intersectedMt.getSortedLowerValueList(globalClock);
                    const QList<QPair<ColorSet, BasicTime> > iterateCandidates
                    = intersectedMt.getSortedHigherValueList(globalClock);

                    for (int i = 0; i < randomCandidates.size() &&
                        !bindable; ++i)
                    {
                        int index = BAH->randomMultisetValue(
                            randomCandidates.size()) + 1;

                        while (BAH->checkBitInBitArray(bitarray, index))
                        {
                            index = BAH->randomMultisetValue(
                                intersectedMt.size());
                        }

                        ColorSet value = randomCandidates.at(index - 1).first;

                        binding.addBoundVariable(holder.m_var,
                            *value.getType());

                        bool binded = true;

                        foreach (const Arc* arc, holder.m_complexConstraints)
                        {
                            Expression* expr = dynamic_cast<Expression* >(
                                arc->getExpression());
                            expr->setBinding(binding);

                            IMultiset* imt = arc->eval(globalClock);

                            const TimedMultiset* emt = 0;

                            bool isEvaluatedMsSmaller = false;

                            if (imt->isTimed())
                            {
                                emt = dynamic_cast<const TimedMultiset* >(
                                    imt);

                                const TimedMultiset* pmt =
                                    dynamic_cast<const TimedMultiset* >(
                                        arc->getPlace()->getTokens());

                                Q_ASSERT(pmt != 0 && emt != 0);

                                *emt + transitionDelay;

                                isEvaluatedMsSmaller = *emt <= *pmt;

                                delete emt;
                            }
                            else
                            {
                                Q_ASSERT(false); // timed/untimed mismatch
                            }

                            if (isEvaluatedMsSmaller)
                            {
                                binded = binded && true;
                            }
                            else
                            {
                                BAH->setBitInBitArray(bitarray, index);
                                binded = false;

                                binding.removeBoundVariable(holder.m_var);
                                break;
                            }
                        }

                        if (binded)
                        {
                            if (transition->getGuard() != 0)
                            {
                                Expression* expr = dynamic_cast<Expression* >(
                                    transition->getGuard());
                                expr->setBinding(binding);

                                _proposedGlobalClock = globalClock;
                                _proposedGlobalClock.add(
                                    transitionDelay.getTime());

                                bindable = transition->check();
                            }
                            else
                            {
                                bindable = true;
                            }
                        }
                    }

                    delete[] bitarray;

                    if (!bindable)
                    {
                        for (int i = 0; i < iterateCandidates.size() &&
                            !bindable; ++i)
                        {
                            ColorSet value = iterateCandidates.at(i).first;
                            binding.addBoundVariable(holder.m_var,
                                *value.getType());

                            bool binded = true;

                            foreach (const Arc* arc,
                                holder.m_complexConstraints)
                            {
                                Expression* expr = dynamic_cast<Expression* >(
                                    arc->getExpression());
                                expr->setBinding(binding);

                                IMultiset* imt = arc->eval(globalClock);

                                const TimedMultiset* emt = 0;

                                bool isEvaluatedMsSmaller = false;

                                if (imt->isTimed())
                                {
                                    emt = dynamic_cast<const TimedMultiset* >(
                                        imt);

                                    const TimedMultiset* pmt =
                                        dynamic_cast<const TimedMultiset* >(
                                            arc->getPlace()->getTokens());

                                    Q_ASSERT(pmt != 0 && emt != 0);

                                    const TimedMultiset _emt = *emt +
                                        transitionDelay;

                                    isEvaluatedMsSmaller = _emt <= *pmt;

                                    delete emt;

                                }
                                else
                                {
                                    Q_ASSERT(false); // timed/untimed mismatch
                                }

                                if (isEvaluatedMsSmaller)
                                {
                                    binded = binded && true;
                                }
                                else
                                {
                                    binded = false;
                                    binding.removeBoundVariable(holder.m_var);
                                    break;
                                }
                            }

                            if (binded)
                            {
                                if (transition->getGuard() != 0)
                                {
                                    Expression* expr =
                                        dynamic_cast<Expression* >(
                                            transition->getGuard());
                                    expr->setBinding(binding);

                                    bindable = transition->check();
                                }
                                else
                                {
                                    bindable = true;
                                }

                                if (bindable)
                                {
                                    if (iterateCandidates.at(i).second >
                                        proposedGlobalClock)
                                    {
                                        proposedGlobalClock =
                                            iterateCandidates.at(i).second;
                                    }
                                }
                            }
                        }
                    }
                    else
                    {
                        if (_proposedGlobalClock > proposedGlobalClock)
                        {
                            proposedGlobalClock = _proposedGlobalClock;
                        }
                    }
                }
                else
                {
                    ret = false;
                    break;
                }
            }
        }
    }

    return ret;
}
